{
 "cells": [
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "from pyeda.inter import *"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "X = exprvars('x', 8, 8)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "R = And(*[OneHot(*[X[r,c] for c in range(8)]) for r in range(8)])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "C = And(*[OneHot(*[X[r,c] for r in range(8)]) for c in range(8)])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "starts = [(i, 0) for i in range(8-2, 0, -1)] + [(0, i) for i in range(8-1)]\n",
    "lrdiags = []\n",
    "for r, c in starts:\n",
    "    lrdiags.append([])\n",
    "    ri, ci = r, c\n",
    "    while ri < 8 and ci < 8:\n",
    "        lrdiags[-1].append((ri, ci))\n",
    "        ri += 1\n",
    "        ci += 1\n",
    "\n",
    "DLR = And(*[OneHot0(*[X[r,c] for r, c in diag]) for diag in lrdiags])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "starts = [(i, 8-1) for i in range(8-2, -1, -1)] + [(0, i) for i in range(8-2, 0, -1)]\n",
    "rldiags = []\n",
    "for r, c in starts:\n",
    "    rldiags.append([])\n",
    "    ri, ci = r, c\n",
    "    while ri < 8 and ci >= 0:\n",
    "        rldiags[-1].append((ri, ci))\n",
    "        ri += 1\n",
    "        ci -= 1\n",
    "\n",
    "DRL = And(*[OneHot0(*[X[r,c] for r, c in diag]) for diag in rldiags])"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "S = And(R, C, DLR, DRL)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "S.is_cnf()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "len(S.xs)"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "def display(point):\n",
    "    chars = list()\n",
    "    for r in range(8):\n",
    "        for c in range(8):\n",
    "            if point[X[r,c]]:\n",
    "                chars.append(\"Q\")\n",
    "            else:\n",
    "                chars.append(\".\")\n",
    "        if r != 7:\n",
    "            chars.append(\"\\n\")\n",
    "    print(\"\".join(chars))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "display(S.satisfy_one())"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "for i, soln in enumerate(S.satisfy_all()):\n",
    "    print(\"Solution\", i+1, end=\"\\n\\n\")\n",
    "    display(soln)\n",
    "    print(\"\")"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "S.satisfy_count()"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": false
   },
   "outputs": [],
   "source": [
    "len(list(S.satisfy_all()))"
   ]
  },
  {
   "cell_type": "code",
   "execution_count": null,
   "metadata": {
    "collapsed": true
   },
   "outputs": [],
   "source": []
  }
 ],
 "metadata": {
  "kernelspec": {
   "display_name": "Python 3",
   "language": "python",
   "name": "python3"
  },
  "language_info": {
   "codemirror_mode": {
    "name": "ipython",
    "version": 3
   },
   "file_extension": ".py",
   "mimetype": "text/x-python",
   "name": "python",
   "nbconvert_exporter": "python",
   "pygments_lexer": "ipython3",
   "version": "3.4.3"
  }
 },
 "nbformat": 4,
 "nbformat_minor": 0
}
